Type inference in 13.11, local declarations, exception monitoring at tag level, and function extensionality

by Colin Adams (modified: 2014 Feb 14)

Several topics here, all arising from my thinking about ISE's proposals for type inference.

Type inference in functional languages such as Haskell, goes naturally with a language where you do not have a locals declaration block. This goes against Eiffel style, so I think type inference should be confined to Eiffel Studio (a sort of extended intellisense).

Thinking about it, I realized we can already dispense with local declarations in 13.11 (and for some considerable time before that).

Haskell has a wonderful program called QuickCheck. It is a bit like our Autotest, except instead of operating on contracts, it operates on QuickCheck properties. These can express general algebraic laws, whcih can't be written in Haskell. As a result, the programmer has to write these laws aside from the source code. Not so good.

Wouldn't it be great if we could use class invariants for checking algebraic laws? Maybe even prove two versions of a function are extensionally equal (then we can laugh even louder at {FUNCTION}.is_equal)? I always thought it was impossible until now:

note description: "Testing type-inference in 13.11" class TEST create execute feature {NONE} -- Initialization execute is -- Test invariant.. do Current.do_nothing -- such a lie! end feature -- Equivalent functions twice_plus_one (a_natural: NATURAL_8): NATURAL -- Twice `a_natural' + 1; -- Uses traditional Eiffel style. local l_plus_one: NATURAL do l_plus_one := a_natural + {NATURAL} 1 Result := 2 * l_plus_one end twice_plus_one_take_2 (a_natural: NATURAL_8): NATURAL -- Twice `a_natural' + 1; -- Uses limited type-inference present in EiffelStudio 13.11. No local declarations. do check attached (a_natural + {NATURAL} 1) as l_plus_one then Result := 2 * l_plus_one end end feature {NONE} -- Facilities inheritance by-pass shared_naturals: NATURAL_8 -- For access to minimum and maximum values once ("PROCESS") create Result end invariant equivalent_functions: across (shared_naturals.Min_value |..| shared_naturals.Max_value) as i_natural all twice_plus_one_take_2 (i_natural.item.as_natural_8) = twice_plus_one (i_natural.item.as_natural_8) end end

Now, this is using the creation procedure to check the invariant clauses. This could easily get very expensive (which is why I used NATURAL_8 rather than NATURAL). What we really want is invariants that are monitored by Autotest, but not by our normal workbench-mode debugging runs.

Eric Bezault has long advocated being able to selectively monitor assertions by selecting on the tag (a regular expression to select tags would be nice). I've always thought this to be an excellent idea - we need it. And this example feeds fuel to the fire, I think.

Comments

Alexander Kogtenkov (10 years ago 14/2/2014)
Shouldn't it be lifted as a postcondition?

It's not clear whether a class invariant is a good choice (not only in this example, but also in general). I believe in many cases it can be expressed as a postcondition instead. The class invariants may be good when they can be violated. If they cannot be violated, they express stricter properties and therefore may be expressed in the stricter form of postconditions. In this example, the postcondition of twice_plus_one_take_2 will be ensure Result = twice_plus_one (a_natural) And this does not seem too expensive now compared to the class invariant case.
- Colin Adams (10 years ago 14/2/2014)
  True. But the postcondition
  
  True. But the postcondition only gets checked on specific values that it gets called on. AutoTest can check values at random. The class I coded tests all possible values, and this technique is available for all functions where the domain can be exhaustively enumerated in a reasonable time.
  
  Anyway, that was merely an after-thought that occured to me as I started to write a demo that local blocks aren't needed. Not that I approve of the style.
  - Alexander Kogtenkov (10 years ago 15/2/2014)
    It depends what class invariant is about
    
    I think a class invariant is about properties of an object. The postcondition better reflects the properties of the features instead. In your example, the argument type can be easily changed into a formal generic type (e.g., NUMERIC) if the property we talk about is coded in the postcondition. But it cannot be expressed in the invariant in this case. In this sense the postconditions are more universal as they apply to all possible argument values even if they cannot be finitely enumerated.
    
    In fact, as soon as the compiler (or some other tool) detects that there is a postcondition that applies to the finite number of argument values, it can automatically add an invariant clause that performs the iteration over all these values.
    - Colin Adams (10 years ago 17/2/2014)
      That's a nice idea.